COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00003 00003	Introduction and Motivation
C00006 00004	.skip 2
C00015 00005		We consider %2recursive programs%1 of the form
C00028 00006	.skip 2
C00031 00007	.if false then begin
C00034 00008	.if false then begin
C00035 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.font B "zero30"
.AT "qt" ⊂"%At%*"⊃
.AT "qf" ⊂"%Af%*"⊃
.AT "qw" ⊂"%8T%*"⊃
.at "Goedel" ⊂"G%B:%*odel"⊃
.at "q≤" ⊂"%8b%*"⊃
.at "q≥" ⊂"%8d%*"⊃
.select 1
.if false then begin
Revisions of Representing Recursive Programs in First Order Logic

1. Corky as co-author

2. Alternate complete recursive program

3. improve treatment of non-recursive representation

4. reference POPL paper

5. emphasize verification technique rather than theorems
.end
Introduction and Motivation

	This paper advances two aspects of the study of the
properties of computer programs - the scientifically motivated search for
general theorems that permit deducing properties of programs and the
engineering problem of replacing debugging by computer-assisted
computer-checked proofs that programs have desired properties.
Both tasks require mathematics, but the second also requires keeping
a non-mathematical goal in mind.  In particular, it is easy for the
theorist to neglect to give an estimate of the range of applicability of
his theorems and examples that show how to use them.

	Cartwright (1976) shows how a recursive program (as in
pure Lisp) defines a function in a first order theory.  The function
satisfies a %2functional equation%1 trivially obtained from
the program, and if the program always terminates, the functional
equation has a unique solution.  One result of this paper shows that
supplementing the %2functional equation%1 by a %2minimization
schema%1.  As is shown in (Cartwright and McCarthy 1979) this completes
the characterization of recursively defined programs.  Namely, given
the functional equation and minimization schema, any sentence involving
the function defined by
the program can be proved within first order logic to be equivalent
to a sentence not involving the function, i.e. a sentence in the data
domain.  Therefore, inability to prove or disprove termination is
just a matter of the Goedelian incompleteness and undecideability
of the data domain.  (It is required that the data domain have enough
functions for elementary syntax).

	While we shall prove some theoretical results and cite others,
the main content of this paper is a discussion of the application of
these new methods to the verification of recursive programs.
.skip 2
Two Inessential Extensions to First Order Logic.

	We begin by extending first order logic to include conditional
expressions and first order λ-expressions.
Translating recursive programs into logical sentences could
be accomplished without these extensions,
but the resulting sentences would often be
much longer than the programs and their relation to the program would be
obscured.  Since we are creating tools for proving properties of actual
programs, we must face the fact that useful programs are quite long enough
as it is.  Obscuring their content in the course of translating them into
logic might make program proving impractical or at least much more
difficult.  On the other hand, we cannot add arbitrary programming
constructions to first order logic without risking its useful properties
such as completeness.  Fortunately, these are harmless
and generally useful extensions.  In fact, they
are useful for expressing mathematical ideas concisely and understandably
quite apart from applications to computer science.  The reader is assumed
to know about first order logic, conditional expressions and
λ-expressions; we explain only their connection.

	Remember that the syntax of first order logic is given in the
form of recursive rules for the formation of terms and wffs.  The
rule for forming terms is extended as follows:

	If ⊗p is a wff and ⊗a and ⊗b are terms, then %2IF p THEN a ELSE b%1
is a term.  Sometimes parentheses must be added to insure unique decomposition.

	The semantics of conditional expression terms is given by a rule for
determining their values.  Namely, if ⊗p is true, the the value of
%2IF p THEN a ELSE b%1 is the value of ⊗a.  Otherwise it is the value
of ⊗b. 

	It is also necessary to add rules of inference to the logic concerned
with conditional expressions.  One could get by with rules permitting
the elimination of conditional expressions from sentences and their
introduction.  These rules are important anyway, because they permit
proof of the metatheorem that the main properties of first order logic
are unaffected by the addition of conditional expressions.  These include
completeness, the deduction theorem, and semi-decidability.

	In order to state these rules it is convenient to introduce
conditional expressions also as a ternary logical connective.  A more fastidious
exposition would use a different notation for logical conditional expressions, but
we will use them so little that we might as well use the same notation,
especially since it is not ambiguous.  Namely, if ⊗p, ⊗q, and ⊗r are
wffs, then so is %2IF p THEN q ELSE r%1.  Its semantics is given by
considering it as a synonym for %2((p ∧ q) ∨ (¬p ∧ r))%1.  Elimination
of conditional expressions is made possible by the distributive laws

!!z1:	%2f(IF p THEN a ELSE b) = IF p THEN f(a) ELSE f(b)%1

and
.begin nofill

!!z2:	%2P(IF p THEN a ELSE b) ∂(35) ≡ IF p THEN P(a) ELSE P(b)%1

∂(35) ≡ (p ∧ P(a)) ∨ (¬p ∧ P(b))%1
.end

where ⊗f and ⊗P stand for arbitrary function and predicate symbols
respectively.  Corresponding distributive rules are needed for functions and
predicates of several arguments when one of the arguments is
a conditional expression.

	Notice that this addition to the logic has nothing to do with
partial functions or the element qw.

	While the above rules are sufficient to preserve the completeness
of first order logic, proofs are often greatly shortened by using the
additional rules introduced in (McCarthy 1963).  We mention especially an
extended form of the rule for replacing an expression by another
expression proved equal to it.  Suppose we want to replace the expression
⊗c by an expression ⊗c' within the conditional expression %2IF p THEN a
ELSE b%1.  To replace an occurrence of ⊗c within ⊗a, we need
not prove %2c_=_c'%1 but merely %2p_⊃_c_=_c'%1.  Likewise if we want to
replace an occurrence of ⊗c in ⊗b, we need only prove %2¬p_⊃_c_=_c'%1.
This principle is further extended in the afore-mentioned paper.

	A further useful and eliminable extension to the logic is
to allow "first order" λ-expressions as function and predicate expressions.
Thus if ⊗x is an individula variable, ⊗e is a term,
and ⊗p is a wff, then %2λx.e%1 and %2λx.p%1
may be used wherever a function symbol or predicate symbol respectively
are allowed.  The only rule required is lambda conversion which serves to
eliminate or introduce λ-expressions.  (We assume that the rules for
λ-conversion include alphabetic changes of bound variables when needed
to avoid capture of the free variables in arguments of λ-expressions.

	The use of minimization
schemata and schemata of induction is facilitated by first order
λ-exressions, since the substitution just replaces occurrences of the
function variable in the schema by a λ-expression which can subsequently
be expanded by λ-conversion.  Without λ-expressions the rule for
substitution in schemata is complicated to state.  First order λ-expressions
also permit many sentences to be expressed more compactly as well as
being required to avoid duplicate computations in recursive programs.
Thus we can write %2[λx.x↑2_+_x](a_+_b)%1 instead of
%2(a_+_b)↑2_+_(a_+_b)%1.  Since all occurrences of first order
λ-expressions can be eliminated from wffs by lambda conversion,
the metatheorems of first order logic are again preserved.  The
reason we don't get the full lambda calculus is that the syntactic
rules of first order logic prevent a variable from being used in
both term and function positions.  While we have illustrated the
use of λ-expressions with single variable λ's,
expressions like %2λx_y_z.e%1 are also useful and give no trouble.
	We consider %2recursive programs%1 of the form

!!g1:	%2f(x) ← %At%*[f](x)%1,

where %At%* is a %2computable functional%1 like

!!g2:	%2%At%* = λf.λx.(qif x = 0 qthen 1 qelse x . f(x - 1))%1,

which gives rise to the well known recursive definition of the factorial
function, namely




.bb "#. The Functional Equation of a Recursive Program."

	Consider the Lisp program

!!h1:	%2subst[x,y,z] ← qif qat z qthen [qif z=y qthen x qelse z]
qelse subst[x,y,qa z] . subst[x,y,qd z]%1.

The above is in Lisp %2external%1 or %2publication%1 notation in
which _qa_%2x%1_ (bold face qa) stands for %2car[x]%1,
_qd_%2x%1_ for %2cdr[x]%1, _%2x_._y%1_
for %2cons[x,y]%1, _qat_%2x%1_ for %2atom[x]%1, _qn_%2x%1_ for %2null[x]%1, and
%2<x%41%2 ... x%4n%1> for %2list[x%41%2, ... ,x%4n%1], and
%2x_*_y%1 for %2append[x,y]%1.  Equality is taken as equality of
S-expressions so that qeq is not used.  The program is written

	(DE SUBST (X Y Z) (COND ((ATOM Z) (COND ((EQUAL Z Y) X) (T Z)))
(T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))

in Lisp %2internal notation%1.

	The basic functions α{%2car, cdr, cons, atomα}%1 of Lisp are all
assumed total, but we will say nothing about the values of ⊗car and
⊗cdr when applied to atoms.  According to the fixed point theory of
recursive programs, any such program defines a function ⊗f from ⊗Sexp (the
set of S-expressions) to Sexp%5+%* (the set of S-expressions augmented
by qw).  This function can be computed by any %2safe computation rule%1,
(in the terminology of Manna, Ness, and Vuillemin (1973)),
and when the computation terminates, its value will belong to ⊗Sexp.  When
the computation doesn't terminate, we postulate %2f(x)_=_qw%1.  Although
the particular function %2subst%1 always terminates,
our first order formula doesn't assume it.  Instead, the first
order formula ({eq h2}) below is the starting point of
a structural induction proof that %2subst%1 is total.

	These facts show that the function %2subst%1 defined recursively
by ({eq h1}) satisfies the sentence

!!h2:	%2∀x y z.(subst(x,y,z) = qif qat z qthen (qif z = y qthen x qelse z)
qelse subst(x,y,qa z) . subst(x,y,qd z))%1

of first order logic.  The variables %2x, y%1 and %2z%1 range over ⊗Sexp; 
when we want to quantify over %2Sexp%5+%1, we use %2X, Y %1and%2 Z%1.
Moreover, we are augmenting first order logic,
as described in (Manna 1974),
by allowing conditional
expressions as terms.  The augmentation does not change what
can be expressed in first order logic, because
conditional expressions can always be eliminated from sentences by
distributing predicates over them.  Thus ({eq h2}) can be written

!!h3:	%2∀x y z.(qat z ⊃ (z=y ⊃ subst(x,y,z) = x) ∧ z≠y ⊃ subst(x,y,z) = z)
∧ ¬qat z ⊃ subst(x,y,z) = subst(x,y,qa z) . subst(x,y,qd z)),%1

but we will use conditional expressions, because they are clearer and
express the recursive program directly.  Indeed, we recommend
their use as terms in logic generally, and in first order logic in
particular.  They don't extend the logical power, but they permit many
facts to be expressed without circumlocution.

	One goal of our first order representation is to use ({eq h1})
only to justify writing ({eq h2}) and then prove all properties of
%2subst%1 using a first order axiomatization of Lisp.
.skip 2





.bb "#. First Order Axioms for Lisp."

	We use lower case variables ⊗x, ⊗y, and ⊗z with or without
subscripts to range over S-expressions.  Capitalized variables
range over all entities.  We also use variables ⊗u, ⊗v and ⊗w with
or without subscripts to range over lists, i.e. S-expressions
such that successive %2cdr%1s eventually reach NIL.  (The %2car%1 of
a list is not required to be a list).  We use predicates %2issexp%1
and %2islist%1 to assert that an individual is an S-expression or
a list.  First come the "housekeeping" and "algebraic" axioms:

L1:	%2∀x.issexp x%1

L2:	%2∀u.islist u%1

L3:	%2∀u.issexp u%1

L4:	%2¬issexp qw

L5:	%2islist %1NIL

L6:	%2qat qNIL%1

L7:	%2∀u.(qat u ⊃ u = qnil)%1

L8:	%2∀x y.issexp (x.y)%1

L9:	%2∀x u.islist (x.u)%1

L10:	%2∀x. ¬qat x ⊃ issexp qa x%1

L11:	%2∀x. ¬qat x ⊃ issexp qd x%1

L12:	%2∀u. u ≠ qNIL ⊃ islist qd u%1

L13:	%2∀x y. qa (x.y) = x%1

L14:	%2∀x y. qd (x.y) = y%1

L15:	%2∀x y. ¬qat (x.y)%1

L16:	%2∀x.¬qat x ⊃ (qa x . qd x) = x%1

	Next we have axiom schemata of induction

LS1:	%2(∀x.qat x ⊃ %AF%* x) ∧ ∀x.(¬qat x ∧ %AF%* qa x ∧ %AF%* qd x ⊃ %AF%* x) ⊃ ∀x.%AF%* x%1

LS2:	%2(∀u.u = qnil ⊃ %AF%* u) ∧ ∀u.(u ≠ qnil ∧ %AF%* qd u ⊃ %AF%* u) ⊃ ∀u. %AF%* u%1.

	From these axioms and schemata, we can prove

!!h4:	%2∀x y z.issexp subst(x,y,z)%1

which is our way of saying that %2subst%1 is total.
The key step is applying the axiom schema LS1 with the
predicate %2%AF%*(z) ≡ issexp subst(x,y,z)%1.
We can also prove
in first order logic
such algebraic properties of %2subst%1 as

!!h5:	%2∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) =
subst(x,y,subst(z,y1,z1)))%1

if we have suitable axiomatization of the predicate %2occur(x,y)%1 meaning
that the atom ⊗x occurs in the S-expression ⊗y. 

	The axiomatization of the predicate %2occur%1 raises some new
problems.  It is defined by the recursive Lisp program

!!h6:	%2occur(x,y) ← (x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y)))%1.

If we were sure in advance that %2occur%1 were total, we could translate
the recursion ({eq h6}) into the sentence

!!h7:	%2∀x y.(occur(x,y) ≡
(x = y) ∨ (¬qat y ∧ (occur(x,qa y) ∨ occur(x,qd y))))%1

which will suffice for proving ({eq h5}), but we
have no right to write it down from the recursive definition ({eq h6}).

	What we may write without proving that %2occur%1 is total
is an implicit definition

!!h8:	%2∀x y.(occura(x,y) =
(x equals y) or (not atom y and (occura(x,qa y) or occura(x,qd y))))%1

and

!!h9:	%2∀x y.(occur(x,y) ≡ (occura(x,y) = T))%1.

From ({eq h8}), we can prove that %2occura%1 is total by structural induction
and from this
({eq h7}) quickly follows.

	Since recursive definitions give rise to partial predicates,
and we don't want to use a partial predicate logic, we introduce a domain
%AP%1 of %2extended truth values%1 with characteristic predicate %2isetv%1
whose elements are ⊗T, ⊗F and qw.
There is no harm in identifying ⊗T and ⊗F with suitable Lisp atoms or
with the integers 1 and 0.
The following axioms describe
functions into or out of %AP%1.  We use the predicate %2istv%1 to test for
the honest truth values ⊗T and ⊗F. 

B0:	%2isetv qw ∧ istv T ∧ istv F%1

B1:	%2∀p.(isetv p)%1

B2:	%2∀p.(p = T ∨ p = F ∨ p = qw)%1

B3:	%2T ≠ F ∧ T ≠ qw ∧ F ≠ qw%1

B4:	%2∀p.(istv p ≡ p = T ∨ p = F)%1

B5:	%2∀p. isetv not p%1

B6:	%2∀p q. isetv(p and q)%1

B7:	%2∀p q. isetv(p or q)%1

B8:	%2∀p.(not p =
qif (p = qw) qthen qw qelse qif p = T qthen F qelse T)%1

B9:	%2∀p q.(p and q =
qif (p = qw) qthen qw qelse qif p = T qthen q qelse F)%1

B10:	%2∀p q.(p or q =
(qif p = qw) qthen qw qelse qif p = T qthen T qelse q)%1

B11:	%2∀X Y.(X equal Y = qif ¬issexp X ∨ ¬issexp Y qthen qw qelse qif
X = Y qthen T qelse F)%1

B12:	%2∀X.(aatom X =
qif ¬issexp X qthen qw qelse qif qat X qthen T qelse F)%1,

and we also need a conditional expression that can take an argument from %AP%1,
namely

B13:	%2∀p X Y.(if(p,X,Y) = qif p = qw qthen qw qelse qif p = T qthen X
qelse Y)%1.

	%2occura%1 is proved total by applying schema LS1 with
%2%AF%*(y) ≡ istv occura(x,y)%1.  After this %2occur%1 can be shown to
satisfy ({eq h7}).

	The axioms L1-L16 and B1-B12 together with the sentences arising
from the schemata LS1 and LS2 will be called the axiom system Lisp0.  We
will adjoin one more axiom later to get the system Lisp1.

	The above method of replacing a recursion by a first order
sentence was first (I think) used in (Cartwright 1976).  I'm
surprised that it wasn't invented sooner.

.skip 1
.indent 0,0;
.skip 2
Axioms for Lisp

	Axioms for Lisp are most concisely expressed in a sorted logic,
and the FOL axiomatizations use sorts.  However, because
unsorted logic is more familiar, we will use it at the cost of somewhat
longer axioms.  Also we won't assume that the only objects are
extended S-expressions, so this axiomatization is suitable for use
when there are other entities involved in the proofs.

L1:	%2∀x y.(issexp x ∧ issexp y ⊃ issexp(x . y) ∧ ¬isatom(x . y) ∧ qa (x.y) = x ∧ qd(x.y) = y)%1

L2:	%2∀x.(issexp x ∧ ¬isatom x ⊃ issexp qa x ∧ issexp qd x ∧ qa x . qd x = x)%1

L3:	%2∀u.(islist u ⊃ issexp u)%1
	
L4:	%2∀u.(u = qNIL ≡ isatom u ∧ islist u)%1

L5:	%2∀u.(islist u ≡ u = qNIL ∨ islist qd u)%1

L6:	%2¬issexp qw%1

L7:	%2∀x.(qw . x = qw ∧ x . qw = qw ∧ qa qw = qw ∧ qd qw = qw)%1

L8:	%2∀x.(issexp x ⊃ qat x = IF x = qw THEN qw ELSE IF isatom x THEN T ELSE F)%1

	The predicate %2occur[x,y]%1 ( which may be read "⊗x occurs in %2y%1" and
defined by the Lisp program

	%2occur[x,y] ← x=y ∨ ¬qat y ∧ [occur[x,qa y) ∨ occur[x,qd y]]%1

gives a partial ordering on S-expressions that can be used to prove
termination and is also used in representing recursively defined
functions non-recursively in section 12.  We will write %2x_≤_y%1 instead
of %2occur[x,y]%1 and axiomatize it by

L9:	%2∀x y.(issexp x ∧ issexp y ⊃ x ≤ y ≡ x = y ∨ (¬isatom y ∧ (x ≤ qa y ∨ x ≤ qd y)))%1

L10:	%2∀x y.(x < y ≡ x ≤ y ∧ x ≠ y)%1

	With the aid of this partial ordering we can give a "course of values"
scheme for structural induction on S-expressions.
We will discuss induction more systematically later.

L11:	%2∀x.(issexp x ∧ ∀y.(issexp y ∧ y < x ⊃ qF(y)) ⊃ qF(x)) ⊃ ∀x.(issexp x ⊃ qF(x))%1

	A corresponding induction principle for lists is given by

L12:	%2∀u.(islist u ∧ ∀y.(islist v ∧ v sublist u ⊃ qF(v)) ⊃ ∀u.(islist u ⊃ qF(u))%1.
.if false then begin
spare text

	In general, we shall be interested in partial functions from a
domain D1 to a domain D2.  We augment these
domains by an undefined element called qw (read "bottom")
giving rise to domains D1%5+%*
and D2%5+%*.  A set ⊗F of total base functions on the domains is assumed
available, and we study functions %2computable from the set F%1
as in (McCarthy 1963).

	We begin by relating the scientific activity of discovering
general theorems that permit deducing properties of computer programs
to the engineering problem of replacing debugging by computer assisted
computer checked proofs that programs have desired properties.
While these enterprises reinforce one another, they have
different motivations and different criteria for success.

	Formalisms for expressing and proving properties of programs
are interesting from two points of view.  First programs are interesting
mathematical objects, and many interesting mathematical theories of
properties have been developed since 1960 with many interesting connections
to older formalisms of recursive function theory.  Second, there is
the applied goal (McCarthy 1960) of replacing debugging by the
routine use of computer assisted and computer checked proofs that
programs meet their specifications.  It may be worthwhile to point out
some relations between these enterprises.
.end
.if false then begin
notes

ok[w,tau] ← qn w ∨ [qda w = tau[λx.ass1[qd w, x]][qaa w] ∧ ok[qd w,tau]]

or non-recursively

ok[w,tau] ≡ ∀u. (u istail w ⊃ [qn u ∨ qaa u = tau[λx.ass1[x,qd u]](qda u)).

y = f(x) ≡ ∃w.(ok(w,tau) ∧ y = tau[λx. ass1[x,w]](x))

Here

	ass1[x,w] ← qif x = qaa w qthen qda w qelse ass1[x, qd w]

or non-recursively

	y = ass1[x,w] ≡ ∃u.(u istail w ∧ x = qaa u ∧ y = qda u).
.end